#include "Heap.cuh"

//// var_indexed_vector class

__device__ var_indexed_vector::var_indexed_vector(int number_of_variables)
{
	this->number_of_variables = number_of_variables;
	this->size = number_of_variables*2;
	indices = (unsigned int*) malloc(sizeof(unsigned int)*size);
	vector = (weighed_literal*) malloc(sizeof(weighed_literal)*size);

	for(int i = 0; i < number_of_variables; i++)
	{
		Lit lpos = mkLit(i, true);
		Lit lneg = mkLit(i,false);
		int pos_index = i*2;
		int neg_index = i*2+1;
		indices[lpos.x] = pos_index;
		indices[lneg.x] = neg_index;

		weighed_literal wlpos, wlneg;
		wlpos.literal = lpos;
		wlpos.weight = 0;
		wlneg.literal = lneg;
		wlneg.weight = 0;

		vector[pos_index] = wlpos;
		vector[neg_index] = wlneg;
	}

}
__device__ void var_indexed_vector::increment(int index, int increment)
{
	vector[index].weight += increment;
}

__device__ int var_indexed_vector::get_size()
{
	return size;
}
__device__ weighed_literal var_indexed_vector::get_weighed_literal(Lit literal)
{
	return vector[literal.x];
}

__device__ bool var_indexed_vector::is_free(Lit literal)
{
	weighed_literal wl = get_weighed_literal(literal);
	return wl.free;
}
__device__ void var_indexed_vector::set_free(Lit literal, bool free)
{
	int index = get_index(literal);
	vector[index].free = free;
}

__device__ weighed_literal var_indexed_vector::get_weighed_literal(int index)
{
	return vector[index];
}

__device__ int var_indexed_vector::get_index(Lit literal)
{
	return indices[literal.x];
}
__device__ void var_indexed_vector::swap(unsigned int index_1, unsigned int index_2)
{
	weighed_literal aux = vector[index_1];
	vector[index_1] = vector[index_2];
	vector[index_2] = aux;

	indices[vector[index_1].literal.x] = index_1;
	indices[vector[index_2].literal.x] = index_2;
}

__device__ void var_indexed_vector::print()
{
	printf("Indices[%d] = {", size);
	for(int i = 0; i < size; i++)
	{
		Lit l;
		l.x = i;

		print_lit(l);
		printf(" = (%d) ", indices[i]);
	}
	printf("}\nValues[%d] = {", size);
	for(int i = 0; i < size; i++)
	{
		printf("(%d) = ", i);
		vector[i].print();
	}
	printf("}\n");
}
